Expression Types

1. Boolean Logical Expression: Two boolean logic operators OR and AND are supported in PAT using symbol '||' and '&&'  respectivly. The conditional-AND/OR operator performs a logical-AND/OR of its bool operands, but only evaluates its second operand if necessary.  
2. Relational Operators contains the equal and not equal relation asl well as other relations. They are expressed using the following symbols in PAT particularly:
   • Equal     '=='
   • Not Equal     '!='
   • Other Relational operators:     '<', '>', '<=', '>='
3. Arithmatic Operators contains the additive and multiplicative expressions which is represented in the model using '+'/ '-' and '*', '/', '%' (modulo operator).
4. Unary Operators contains '+', '-' for positive or negtive values, '!' for negation of boolean expressions.
5. Increment '++' or Decrement operators '--' increase or decrease the variable by 1 respectively.
6. If Expresson: The conditions in If can be expressions and their conbinations we have introduced above. Then it has the similar meaning and usage as common programming languages. Note that this if expression can only contain expressions in the than or else branches, but the if process in the model can only contains processes in the than or else branches.
7. While Expression: Similar as if expressions, while expression takes expresions of type 1-4 or their combinations as condition and behaves just like it has defined in common programming languages.

Note: Expressions of type 1-5 can be composed to be complex expressions. And this composed expression will be parsed in the priority of 5 to 1 (i.e. the precedence order). For example, if a, b, c are defined as variables, the following complex expression is a valid expression.

if ((a % 2 == 0) || ( ((a++) <= b) && (b == c)) )

Indexed Boolean Expression

The indexed expression is a syntax sugar for grouping a list of OR or AND expressions together overal a range of variables. The syntax is following:

A typical example is as follows:

var x[3];

P =  if(&& i:{0..2}@(x[i] == 0)){bingo -> Skip};

Expression Macro Definition

Users can define expression macro using define keywork and use the macro in the model or assertiosn.

var x;

#define goal x < 0;